Nuprl Definition : ecl-trans-state-from 11,40
ecl-trans-state-from(v; z; L)
== spreadn(v;
== spreadn(T,ks,i,g,h,a,e.list_accum(x,a.let k,zz = a
== spreadn(T,ks,i,g,h,a,e.list_accum(in
== spreadn(T,ks,i,g,h,a,e.list_accum(let s,v = zz
== spreadn(T,ks,i,g,h,a,e.list_accum(in
== spreadn(T,ks,i,g,h,a,e.list_accum(if deq-member(Kind-deq; k; ks) then g(k,s,v,x) else x fi ;
== spreadn(T,ks,i,g,h,a,e.list_accum(z;
== spreadn(T,ks,i,g,h,a,e.list_accum(L)) 
latex

Definitionsspreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), list_accum(x,a.f(x;a); y; l), if b then t else f fi , deq-member(eq; x; L), Kind-deq
FDL editor aliasesecl-trans-state-from

origin